Contents of Interleaving trace semantics

We now investigate whether interleaving equivalences are preserved by safe refinements. We start by considering the simplest notion, the usual interleaving trace equivalence where the possible sequences of actions are compared.

Definition 3.1

w = a₁...a_n∈ $\it Act\/^{*}_{}$ is a (sequential) trace of $\cal {E}$ ∈ IE iff
∃X₀,..., X_n∈ $\it Conf\/$ ( $\cal {E}$ ) : X₀ = ∅ and X_i-1 $\buildrel$ a_i $\over$ →X_i , i = 1,..., n.

SeqTraces( $\cal {E}$ ) denotes the set of all sequential traces of $\cal {E}$ .

$\cal {E}$ , $\cal {F}$ ∈ IE are called interleaving trace equivalent ( $\cal {E}$ $\approx_{{it}}^{}$ $\cal {F}$ ) iff
SeqTraces( $\cal {E}$ ) = SeqTraces( $\cal {F}$ ).

The following example shows that this equivalence is not preserved by safe refinements.

Example 3.1

Consider the event structures $\cal {E}$ and $\cal {F}$ below, corresponding to a(b| c) and abc + acb.

$\begin{picture}(149,40)(-10,11) \put(15,44){\makebox(0,0)[b]{${\cal E} =$}} \put... ...{5}} \put(110,28){\line (0,-1){10}} \put(110,28){\vector(0,-1){5}} \end{picture}$

$\cal {E}$ $\approx_{{it}}^{}$ $\cal {F}$ , since the only traces for both event structures are abc and acb (and the prefixes). Action b is not critical. We refine b by b₁b₂.

$\begin{picture}(149,57)(-10,4) \put(15,53){\makebox(0,0)[b]{${\it ref\/}({\cal E... ...{5}} \put(110,22){\line (0,-1){10}} \put(110,22){\vector(0,-1){5}} \end{picture}$

We have $\it ref\/$ ( $\cal {E}$ ) $\not\approx$ _it $\it ref\/$ ( $\cal {F}$ ), since ab₁c∈SeqTraces( $\it ref\/$ ( $\cal {E}$ )),
but ab₁c $\not\in$ SeqTraces( $\it ref\/$ ( $\cal {F}$ )).

One can now ask if it is possible to strengthen the requirement of safe refinements, say into trace-safe refinements, by requiring more actions to be atomic, in such a way that interleaving trace equivalence is preserved under trace-safe refinements. Requiring all actions that can occur concurrently with another action to be atomic would work, but this constraint is very restrictive. It seems not easy to find a less restrictive one.